(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
0(0(1(2(x1)))) → 0(2(1(3(3(0(x1))))))
0(1(0(4(x1)))) → 0(1(3(0(4(x1)))))
0(1(0(5(x1)))) → 0(1(3(5(0(x1)))))
0(1(5(0(x1)))) → 0(1(3(5(0(x1)))))
0(3(1(0(x1)))) → 0(1(3(5(0(x1)))))
3(1(0(2(x1)))) → 1(3(5(0(2(x1)))))
3(1(0(2(x1)))) → 3(2(1(3(0(x1)))))
3(1(0(5(x1)))) → 1(3(5(3(0(x1)))))
3(1(2(0(x1)))) → 2(1(3(3(0(x1)))))
3(1(2(0(x1)))) → 3(0(2(1(4(x1)))))
3(1(2(0(x1)))) → 3(0(3(2(1(x1)))))
3(1(2(0(x1)))) → 3(3(2(1(0(x1)))))
3(1(2(0(x1)))) → 3(5(2(1(0(x1)))))
3(1(2(2(x1)))) → 3(5(2(2(1(x1)))))
3(4(2(0(x1)))) → 3(3(2(4(0(x1)))))
4(0(1(0(x1)))) → 1(3(0(4(0(x1)))))
5(1(0(5(x1)))) → 1(3(3(5(5(0(x1))))))
5(2(5(0(x1)))) → 5(2(3(5(0(x1)))))
5(3(1(0(x1)))) → 0(1(3(5(5(x1)))))
0(0(4(1(0(x1))))) → 0(4(1(3(0(0(x1))))))
0(1(2(0(5(x1))))) → 0(3(0(5(1(2(x1))))))
0(1(3(1(2(x1))))) → 3(0(2(2(1(1(x1))))))
0(1(5(0(4(x1))))) → 0(4(1(3(5(0(x1))))))
0(1(5(3(5(x1))))) → 0(1(3(5(3(5(x1))))))
0(2(0(3(4(x1))))) → 0(4(5(2(3(0(x1))))))
0(2(3(1(5(x1))))) → 0(1(3(5(5(2(x1))))))
0(2(4(1(2(x1))))) → 0(2(1(1(4(2(x1))))))
0(2(5(0(2(x1))))) → 0(0(3(5(2(2(x1))))))
0(2(5(5(0(x1))))) → 0(0(2(5(1(5(x1))))))
0(3(1(5(0(x1))))) → 1(3(0(5(3(0(x1))))))
0(5(3(2(0(x1))))) → 0(0(2(1(3(5(x1))))))
3(1(0(5(2(x1))))) → 2(4(1(3(5(0(x1))))))
3(1(3(0(2(x1))))) → 2(1(3(3(3(0(x1))))))
3(1(3(2(0(x1))))) → 3(1(3(0(5(2(x1))))))
3(1(4(1(2(x1))))) → 1(4(3(2(2(1(x1))))))
3(1(4(2(0(x1))))) → 2(1(3(3(0(4(x1))))))
3(1(5(0(2(x1))))) → 2(5(1(3(0(5(x1))))))
3(3(1(0(0(x1))))) → 5(1(3(3(0(0(x1))))))
3(4(0(2(0(x1))))) → 3(0(0(2(1(4(x1))))))
3(4(2(3(2(x1))))) → 3(3(2(5(4(2(x1))))))
4(3(1(0(2(x1))))) → 4(2(1(3(0(1(x1))))))
4(3(1(2(0(x1))))) → 1(3(0(1(4(2(x1))))))
4(5(5(1(2(x1))))) → 5(4(5(2(1(1(x1))))))
4(5(5(5(0(x1))))) → 5(5(1(5(0(4(x1))))))
5(1(0(1(2(x1))))) → 2(1(1(3(5(0(x1))))))
5(1(1(0(4(x1))))) → 5(1(1(4(3(0(x1))))))
5(1(5(2(0(x1))))) → 2(1(3(5(0(5(x1))))))
5(4(1(0(5(x1))))) → 4(1(3(5(5(0(x1))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(0(1(2(z0)))) → 0(2(1(3(3(0(z0))))))
0(1(0(4(z0)))) → 0(1(3(0(4(z0)))))
0(1(0(5(z0)))) → 0(1(3(5(0(z0)))))
0(1(5(0(z0)))) → 0(1(3(5(0(z0)))))
0(3(1(0(z0)))) → 0(1(3(5(0(z0)))))
0(0(4(1(0(z0))))) → 0(4(1(3(0(0(z0))))))
0(1(2(0(5(z0))))) → 0(3(0(5(1(2(z0))))))
0(1(3(1(2(z0))))) → 3(0(2(2(1(1(z0))))))
0(1(5(0(4(z0))))) → 0(4(1(3(5(0(z0))))))
0(1(5(3(5(z0))))) → 0(1(3(5(3(5(z0))))))
0(2(0(3(4(z0))))) → 0(4(5(2(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(1(3(5(5(2(z0))))))
0(2(4(1(2(z0))))) → 0(2(1(1(4(2(z0))))))
0(2(5(0(2(z0))))) → 0(0(3(5(2(2(z0))))))
0(2(5(5(0(z0))))) → 0(0(2(5(1(5(z0))))))
0(3(1(5(0(z0))))) → 1(3(0(5(3(0(z0))))))
0(5(3(2(0(z0))))) → 0(0(2(1(3(5(z0))))))
3(1(0(2(z0)))) → 1(3(5(0(2(z0)))))
3(1(0(2(z0)))) → 3(2(1(3(0(z0)))))
3(1(0(5(z0)))) → 1(3(5(3(0(z0)))))
3(1(2(0(z0)))) → 2(1(3(3(0(z0)))))
3(1(2(0(z0)))) → 3(0(2(1(4(z0)))))
3(1(2(0(z0)))) → 3(0(3(2(1(z0)))))
3(1(2(0(z0)))) → 3(3(2(1(0(z0)))))
3(1(2(0(z0)))) → 3(5(2(1(0(z0)))))
3(1(2(2(z0)))) → 3(5(2(2(1(z0)))))
3(4(2(0(z0)))) → 3(3(2(4(0(z0)))))
3(1(0(5(2(z0))))) → 2(4(1(3(5(0(z0))))))
3(1(3(0(2(z0))))) → 2(1(3(3(3(0(z0))))))
3(1(3(2(0(z0))))) → 3(1(3(0(5(2(z0))))))
3(1(4(1(2(z0))))) → 1(4(3(2(2(1(z0))))))
3(1(4(2(0(z0))))) → 2(1(3(3(0(4(z0))))))
3(1(5(0(2(z0))))) → 2(5(1(3(0(5(z0))))))
3(3(1(0(0(z0))))) → 5(1(3(3(0(0(z0))))))
3(4(0(2(0(z0))))) → 3(0(0(2(1(4(z0))))))
3(4(2(3(2(z0))))) → 3(3(2(5(4(2(z0))))))
4(0(1(0(z0)))) → 1(3(0(4(0(z0)))))
4(3(1(0(2(z0))))) → 4(2(1(3(0(1(z0))))))
4(3(1(2(0(z0))))) → 1(3(0(1(4(2(z0))))))
4(5(5(1(2(z0))))) → 5(4(5(2(1(1(z0))))))
4(5(5(5(0(z0))))) → 5(5(1(5(0(4(z0))))))
5(1(0(5(z0)))) → 1(3(3(5(5(0(z0))))))
5(2(5(0(z0)))) → 5(2(3(5(0(z0)))))
5(3(1(0(z0)))) → 0(1(3(5(5(z0)))))
5(1(0(1(2(z0))))) → 2(1(1(3(5(0(z0))))))
5(1(1(0(4(z0))))) → 5(1(1(4(3(0(z0))))))
5(1(5(2(0(z0))))) → 2(1(3(5(0(5(z0))))))
5(4(1(0(5(z0))))) → 4(1(3(5(5(0(z0))))))
Tuples:
0'(0(1(2(z0)))) → c(0'(2(1(3(3(0(z0)))))), 3'(3(0(z0))), 3'(0(z0)), 0'(z0))
0'(1(0(4(z0)))) → c1(0'(1(3(0(4(z0))))), 3'(0(4(z0))), 0'(4(z0)), 4'(z0))
0'(1(0(5(z0)))) → c2(0'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(1(5(0(z0)))) → c3(0'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(3(1(0(z0)))) → c4(0'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(0(4(1(0(z0))))) → c5(0'(4(1(3(0(0(z0)))))), 4'(1(3(0(0(z0))))), 3'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(2(0(5(z0))))) → c6(0'(3(0(5(1(2(z0)))))), 3'(0(5(1(2(z0))))), 0'(5(1(2(z0)))), 5'(1(2(z0))))
0'(1(3(1(2(z0))))) → c7(3'(0(2(2(1(1(z0)))))), 0'(2(2(1(1(z0))))))
0'(1(5(0(4(z0))))) → c8(0'(4(1(3(5(0(z0)))))), 4'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(1(5(3(5(z0))))) → c9(0'(1(3(5(3(5(z0)))))), 3'(5(3(5(z0)))), 5'(3(5(z0))), 3'(5(z0)), 5'(z0))
0'(2(0(3(4(z0))))) → c10(0'(4(5(2(3(0(z0)))))), 4'(5(2(3(0(z0))))), 5'(2(3(0(z0)))), 3'(0(z0)), 0'(z0))
0'(2(3(1(5(z0))))) → c11(0'(1(3(5(5(2(z0)))))), 3'(5(5(2(z0)))), 5'(5(2(z0))), 5'(2(z0)))
0'(2(4(1(2(z0))))) → c12(0'(2(1(1(4(2(z0)))))), 4'(2(z0)))
0'(2(5(0(2(z0))))) → c13(0'(0(3(5(2(2(z0)))))), 0'(3(5(2(2(z0))))), 3'(5(2(2(z0)))), 5'(2(2(z0))))
0'(2(5(5(0(z0))))) → c14(0'(0(2(5(1(5(z0)))))), 0'(2(5(1(5(z0))))), 5'(1(5(z0))), 5'(z0))
0'(3(1(5(0(z0))))) → c15(3'(0(5(3(0(z0))))), 0'(5(3(0(z0)))), 5'(3(0(z0))), 3'(0(z0)), 0'(z0))
0'(5(3(2(0(z0))))) → c16(0'(0(2(1(3(5(z0)))))), 0'(2(1(3(5(z0))))), 3'(5(z0)), 5'(z0))
3'(1(0(2(z0)))) → c17(3'(5(0(2(z0)))), 5'(0(2(z0))), 0'(2(z0)))
3'(1(0(2(z0)))) → c18(3'(2(1(3(0(z0))))), 3'(0(z0)), 0'(z0))
3'(1(0(5(z0)))) → c19(3'(5(3(0(z0)))), 5'(3(0(z0))), 3'(0(z0)), 0'(z0))
3'(1(2(0(z0)))) → c20(3'(3(0(z0))), 3'(0(z0)), 0'(z0))
3'(1(2(0(z0)))) → c21(3'(0(2(1(4(z0))))), 0'(2(1(4(z0)))), 4'(z0))
3'(1(2(0(z0)))) → c22(3'(0(3(2(1(z0))))), 0'(3(2(1(z0)))), 3'(2(1(z0))))
3'(1(2(0(z0)))) → c23(3'(3(2(1(0(z0))))), 3'(2(1(0(z0)))), 0'(z0))
3'(1(2(0(z0)))) → c24(3'(5(2(1(0(z0))))), 5'(2(1(0(z0)))), 0'(z0))
3'(1(2(2(z0)))) → c25(3'(5(2(2(1(z0))))), 5'(2(2(1(z0)))))
3'(4(2(0(z0)))) → c26(3'(3(2(4(0(z0))))), 3'(2(4(0(z0)))), 4'(0(z0)), 0'(z0))
3'(1(0(5(2(z0))))) → c27(4'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
3'(1(3(0(2(z0))))) → c28(3'(3(3(0(z0)))), 3'(3(0(z0))), 3'(0(z0)), 0'(z0))
3'(1(3(2(0(z0))))) → c29(3'(1(3(0(5(2(z0)))))), 3'(0(5(2(z0)))), 0'(5(2(z0))), 5'(2(z0)))
3'(1(4(1(2(z0))))) → c30(4'(3(2(2(1(z0))))), 3'(2(2(1(z0)))))
3'(1(4(2(0(z0))))) → c31(3'(3(0(4(z0)))), 3'(0(4(z0))), 0'(4(z0)), 4'(z0))
3'(1(5(0(2(z0))))) → c32(5'(1(3(0(5(z0))))), 3'(0(5(z0))), 0'(5(z0)), 5'(z0))
3'(3(1(0(0(z0))))) → c33(5'(1(3(3(0(0(z0)))))), 3'(3(0(0(z0)))), 3'(0(0(z0))), 0'(0(z0)), 0'(z0))
3'(4(0(2(0(z0))))) → c34(3'(0(0(2(1(4(z0)))))), 0'(0(2(1(4(z0))))), 0'(2(1(4(z0)))), 4'(z0))
3'(4(2(3(2(z0))))) → c35(3'(3(2(5(4(2(z0)))))), 3'(2(5(4(2(z0))))), 5'(4(2(z0))), 4'(2(z0)))
4'(0(1(0(z0)))) → c36(3'(0(4(0(z0)))), 0'(4(0(z0))), 4'(0(z0)), 0'(z0))
4'(3(1(0(2(z0))))) → c37(4'(2(1(3(0(1(z0)))))), 3'(0(1(z0))), 0'(1(z0)))
4'(3(1(2(0(z0))))) → c38(3'(0(1(4(2(z0))))), 0'(1(4(2(z0)))), 4'(2(z0)))
4'(5(5(1(2(z0))))) → c39(5'(4(5(2(1(1(z0)))))), 4'(5(2(1(1(z0))))), 5'(2(1(1(z0)))))
4'(5(5(5(0(z0))))) → c40(5'(5(1(5(0(4(z0)))))), 5'(1(5(0(4(z0))))), 5'(0(4(z0))), 0'(4(z0)), 4'(z0))
5'(1(0(5(z0)))) → c41(3'(3(5(5(0(z0))))), 3'(5(5(0(z0)))), 5'(5(0(z0))), 5'(0(z0)), 0'(z0))
5'(2(5(0(z0)))) → c42(5'(2(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
5'(3(1(0(z0)))) → c43(0'(1(3(5(5(z0))))), 3'(5(5(z0))), 5'(5(z0)), 5'(z0))
5'(1(0(1(2(z0))))) → c44(3'(5(0(z0))), 5'(0(z0)), 0'(z0))
5'(1(1(0(4(z0))))) → c45(5'(1(1(4(3(0(z0)))))), 4'(3(0(z0))), 3'(0(z0)), 0'(z0))
5'(1(5(2(0(z0))))) → c46(3'(5(0(5(z0)))), 5'(0(5(z0))), 0'(5(z0)), 5'(z0))
5'(4(1(0(5(z0))))) → c47(4'(1(3(5(5(0(z0)))))), 3'(5(5(0(z0)))), 5'(5(0(z0))), 5'(0(z0)), 0'(z0))
S tuples:
0'(0(1(2(z0)))) → c(0'(2(1(3(3(0(z0)))))), 3'(3(0(z0))), 3'(0(z0)), 0'(z0))
0'(1(0(4(z0)))) → c1(0'(1(3(0(4(z0))))), 3'(0(4(z0))), 0'(4(z0)), 4'(z0))
0'(1(0(5(z0)))) → c2(0'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(1(5(0(z0)))) → c3(0'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(3(1(0(z0)))) → c4(0'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(0(4(1(0(z0))))) → c5(0'(4(1(3(0(0(z0)))))), 4'(1(3(0(0(z0))))), 3'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(2(0(5(z0))))) → c6(0'(3(0(5(1(2(z0)))))), 3'(0(5(1(2(z0))))), 0'(5(1(2(z0)))), 5'(1(2(z0))))
0'(1(3(1(2(z0))))) → c7(3'(0(2(2(1(1(z0)))))), 0'(2(2(1(1(z0))))))
0'(1(5(0(4(z0))))) → c8(0'(4(1(3(5(0(z0)))))), 4'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(1(5(3(5(z0))))) → c9(0'(1(3(5(3(5(z0)))))), 3'(5(3(5(z0)))), 5'(3(5(z0))), 3'(5(z0)), 5'(z0))
0'(2(0(3(4(z0))))) → c10(0'(4(5(2(3(0(z0)))))), 4'(5(2(3(0(z0))))), 5'(2(3(0(z0)))), 3'(0(z0)), 0'(z0))
0'(2(3(1(5(z0))))) → c11(0'(1(3(5(5(2(z0)))))), 3'(5(5(2(z0)))), 5'(5(2(z0))), 5'(2(z0)))
0'(2(4(1(2(z0))))) → c12(0'(2(1(1(4(2(z0)))))), 4'(2(z0)))
0'(2(5(0(2(z0))))) → c13(0'(0(3(5(2(2(z0)))))), 0'(3(5(2(2(z0))))), 3'(5(2(2(z0)))), 5'(2(2(z0))))
0'(2(5(5(0(z0))))) → c14(0'(0(2(5(1(5(z0)))))), 0'(2(5(1(5(z0))))), 5'(1(5(z0))), 5'(z0))
0'(3(1(5(0(z0))))) → c15(3'(0(5(3(0(z0))))), 0'(5(3(0(z0)))), 5'(3(0(z0))), 3'(0(z0)), 0'(z0))
0'(5(3(2(0(z0))))) → c16(0'(0(2(1(3(5(z0)))))), 0'(2(1(3(5(z0))))), 3'(5(z0)), 5'(z0))
3'(1(0(2(z0)))) → c17(3'(5(0(2(z0)))), 5'(0(2(z0))), 0'(2(z0)))
3'(1(0(2(z0)))) → c18(3'(2(1(3(0(z0))))), 3'(0(z0)), 0'(z0))
3'(1(0(5(z0)))) → c19(3'(5(3(0(z0)))), 5'(3(0(z0))), 3'(0(z0)), 0'(z0))
3'(1(2(0(z0)))) → c20(3'(3(0(z0))), 3'(0(z0)), 0'(z0))
3'(1(2(0(z0)))) → c21(3'(0(2(1(4(z0))))), 0'(2(1(4(z0)))), 4'(z0))
3'(1(2(0(z0)))) → c22(3'(0(3(2(1(z0))))), 0'(3(2(1(z0)))), 3'(2(1(z0))))
3'(1(2(0(z0)))) → c23(3'(3(2(1(0(z0))))), 3'(2(1(0(z0)))), 0'(z0))
3'(1(2(0(z0)))) → c24(3'(5(2(1(0(z0))))), 5'(2(1(0(z0)))), 0'(z0))
3'(1(2(2(z0)))) → c25(3'(5(2(2(1(z0))))), 5'(2(2(1(z0)))))
3'(4(2(0(z0)))) → c26(3'(3(2(4(0(z0))))), 3'(2(4(0(z0)))), 4'(0(z0)), 0'(z0))
3'(1(0(5(2(z0))))) → c27(4'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
3'(1(3(0(2(z0))))) → c28(3'(3(3(0(z0)))), 3'(3(0(z0))), 3'(0(z0)), 0'(z0))
3'(1(3(2(0(z0))))) → c29(3'(1(3(0(5(2(z0)))))), 3'(0(5(2(z0)))), 0'(5(2(z0))), 5'(2(z0)))
3'(1(4(1(2(z0))))) → c30(4'(3(2(2(1(z0))))), 3'(2(2(1(z0)))))
3'(1(4(2(0(z0))))) → c31(3'(3(0(4(z0)))), 3'(0(4(z0))), 0'(4(z0)), 4'(z0))
3'(1(5(0(2(z0))))) → c32(5'(1(3(0(5(z0))))), 3'(0(5(z0))), 0'(5(z0)), 5'(z0))
3'(3(1(0(0(z0))))) → c33(5'(1(3(3(0(0(z0)))))), 3'(3(0(0(z0)))), 3'(0(0(z0))), 0'(0(z0)), 0'(z0))
3'(4(0(2(0(z0))))) → c34(3'(0(0(2(1(4(z0)))))), 0'(0(2(1(4(z0))))), 0'(2(1(4(z0)))), 4'(z0))
3'(4(2(3(2(z0))))) → c35(3'(3(2(5(4(2(z0)))))), 3'(2(5(4(2(z0))))), 5'(4(2(z0))), 4'(2(z0)))
4'(0(1(0(z0)))) → c36(3'(0(4(0(z0)))), 0'(4(0(z0))), 4'(0(z0)), 0'(z0))
4'(3(1(0(2(z0))))) → c37(4'(2(1(3(0(1(z0)))))), 3'(0(1(z0))), 0'(1(z0)))
4'(3(1(2(0(z0))))) → c38(3'(0(1(4(2(z0))))), 0'(1(4(2(z0)))), 4'(2(z0)))
4'(5(5(1(2(z0))))) → c39(5'(4(5(2(1(1(z0)))))), 4'(5(2(1(1(z0))))), 5'(2(1(1(z0)))))
4'(5(5(5(0(z0))))) → c40(5'(5(1(5(0(4(z0)))))), 5'(1(5(0(4(z0))))), 5'(0(4(z0))), 0'(4(z0)), 4'(z0))
5'(1(0(5(z0)))) → c41(3'(3(5(5(0(z0))))), 3'(5(5(0(z0)))), 5'(5(0(z0))), 5'(0(z0)), 0'(z0))
5'(2(5(0(z0)))) → c42(5'(2(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
5'(3(1(0(z0)))) → c43(0'(1(3(5(5(z0))))), 3'(5(5(z0))), 5'(5(z0)), 5'(z0))
5'(1(0(1(2(z0))))) → c44(3'(5(0(z0))), 5'(0(z0)), 0'(z0))
5'(1(1(0(4(z0))))) → c45(5'(1(1(4(3(0(z0)))))), 4'(3(0(z0))), 3'(0(z0)), 0'(z0))
5'(1(5(2(0(z0))))) → c46(3'(5(0(5(z0)))), 5'(0(5(z0))), 0'(5(z0)), 5'(z0))
5'(4(1(0(5(z0))))) → c47(4'(1(3(5(5(0(z0)))))), 3'(5(5(0(z0)))), 5'(5(0(z0))), 5'(0(z0)), 0'(z0))
K tuples:none
Defined Rule Symbols:
0, 3, 4, 5
Defined Pair Symbols:
0', 3', 4', 5'
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
0'(0(1(2(z0)))) → c(0'(2(1(3(3(0(z0)))))), 3'(3(0(z0))), 3'(0(z0)), 0'(z0))
0'(1(0(4(z0)))) → c1(0'(1(3(0(4(z0))))), 3'(0(4(z0))), 0'(4(z0)), 4'(z0))
0'(1(0(5(z0)))) → c2(0'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(1(5(0(z0)))) → c3(0'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(3(1(0(z0)))) → c4(0'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(0(4(1(0(z0))))) → c5(0'(4(1(3(0(0(z0)))))), 4'(1(3(0(0(z0))))), 3'(0(0(z0))), 0'(0(z0)), 0'(z0))
0'(1(2(0(5(z0))))) → c6(0'(3(0(5(1(2(z0)))))), 3'(0(5(1(2(z0))))), 0'(5(1(2(z0)))), 5'(1(2(z0))))
0'(1(3(1(2(z0))))) → c7(3'(0(2(2(1(1(z0)))))), 0'(2(2(1(1(z0))))))
0'(1(5(0(4(z0))))) → c8(0'(4(1(3(5(0(z0)))))), 4'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
0'(1(5(3(5(z0))))) → c9(0'(1(3(5(3(5(z0)))))), 3'(5(3(5(z0)))), 5'(3(5(z0))), 3'(5(z0)), 5'(z0))
0'(2(0(3(4(z0))))) → c10(0'(4(5(2(3(0(z0)))))), 4'(5(2(3(0(z0))))), 5'(2(3(0(z0)))), 3'(0(z0)), 0'(z0))
0'(2(3(1(5(z0))))) → c11(0'(1(3(5(5(2(z0)))))), 3'(5(5(2(z0)))), 5'(5(2(z0))), 5'(2(z0)))
0'(2(4(1(2(z0))))) → c12(0'(2(1(1(4(2(z0)))))), 4'(2(z0)))
0'(2(5(0(2(z0))))) → c13(0'(0(3(5(2(2(z0)))))), 0'(3(5(2(2(z0))))), 3'(5(2(2(z0)))), 5'(2(2(z0))))
0'(2(5(5(0(z0))))) → c14(0'(0(2(5(1(5(z0)))))), 0'(2(5(1(5(z0))))), 5'(1(5(z0))), 5'(z0))
0'(3(1(5(0(z0))))) → c15(3'(0(5(3(0(z0))))), 0'(5(3(0(z0)))), 5'(3(0(z0))), 3'(0(z0)), 0'(z0))
0'(5(3(2(0(z0))))) → c16(0'(0(2(1(3(5(z0)))))), 0'(2(1(3(5(z0))))), 3'(5(z0)), 5'(z0))
3'(1(0(2(z0)))) → c17(3'(5(0(2(z0)))), 5'(0(2(z0))), 0'(2(z0)))
3'(1(0(2(z0)))) → c18(3'(2(1(3(0(z0))))), 3'(0(z0)), 0'(z0))
3'(1(0(5(z0)))) → c19(3'(5(3(0(z0)))), 5'(3(0(z0))), 3'(0(z0)), 0'(z0))
3'(1(2(0(z0)))) → c20(3'(3(0(z0))), 3'(0(z0)), 0'(z0))
3'(1(2(0(z0)))) → c21(3'(0(2(1(4(z0))))), 0'(2(1(4(z0)))), 4'(z0))
3'(1(2(0(z0)))) → c22(3'(0(3(2(1(z0))))), 0'(3(2(1(z0)))), 3'(2(1(z0))))
3'(1(2(0(z0)))) → c23(3'(3(2(1(0(z0))))), 3'(2(1(0(z0)))), 0'(z0))
3'(1(2(0(z0)))) → c24(3'(5(2(1(0(z0))))), 5'(2(1(0(z0)))), 0'(z0))
3'(4(2(0(z0)))) → c26(3'(3(2(4(0(z0))))), 3'(2(4(0(z0)))), 4'(0(z0)), 0'(z0))
3'(1(0(5(2(z0))))) → c27(4'(1(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
3'(1(3(0(2(z0))))) → c28(3'(3(3(0(z0)))), 3'(3(0(z0))), 3'(0(z0)), 0'(z0))
3'(1(3(2(0(z0))))) → c29(3'(1(3(0(5(2(z0)))))), 3'(0(5(2(z0)))), 0'(5(2(z0))), 5'(2(z0)))
3'(1(4(1(2(z0))))) → c30(4'(3(2(2(1(z0))))), 3'(2(2(1(z0)))))
3'(1(4(2(0(z0))))) → c31(3'(3(0(4(z0)))), 3'(0(4(z0))), 0'(4(z0)), 4'(z0))
3'(1(5(0(2(z0))))) → c32(5'(1(3(0(5(z0))))), 3'(0(5(z0))), 0'(5(z0)), 5'(z0))
3'(3(1(0(0(z0))))) → c33(5'(1(3(3(0(0(z0)))))), 3'(3(0(0(z0)))), 3'(0(0(z0))), 0'(0(z0)), 0'(z0))
3'(4(0(2(0(z0))))) → c34(3'(0(0(2(1(4(z0)))))), 0'(0(2(1(4(z0))))), 0'(2(1(4(z0)))), 4'(z0))
3'(4(2(3(2(z0))))) → c35(3'(3(2(5(4(2(z0)))))), 3'(2(5(4(2(z0))))), 5'(4(2(z0))), 4'(2(z0)))
4'(0(1(0(z0)))) → c36(3'(0(4(0(z0)))), 0'(4(0(z0))), 4'(0(z0)), 0'(z0))
4'(3(1(0(2(z0))))) → c37(4'(2(1(3(0(1(z0)))))), 3'(0(1(z0))), 0'(1(z0)))
4'(3(1(2(0(z0))))) → c38(3'(0(1(4(2(z0))))), 0'(1(4(2(z0)))), 4'(2(z0)))
4'(5(5(1(2(z0))))) → c39(5'(4(5(2(1(1(z0)))))), 4'(5(2(1(1(z0))))), 5'(2(1(1(z0)))))
4'(5(5(5(0(z0))))) → c40(5'(5(1(5(0(4(z0)))))), 5'(1(5(0(4(z0))))), 5'(0(4(z0))), 0'(4(z0)), 4'(z0))
5'(1(0(5(z0)))) → c41(3'(3(5(5(0(z0))))), 3'(5(5(0(z0)))), 5'(5(0(z0))), 5'(0(z0)), 0'(z0))
5'(2(5(0(z0)))) → c42(5'(2(3(5(0(z0))))), 3'(5(0(z0))), 5'(0(z0)), 0'(z0))
5'(3(1(0(z0)))) → c43(0'(1(3(5(5(z0))))), 3'(5(5(z0))), 5'(5(z0)), 5'(z0))
5'(1(0(1(2(z0))))) → c44(3'(5(0(z0))), 5'(0(z0)), 0'(z0))
5'(1(1(0(4(z0))))) → c45(5'(1(1(4(3(0(z0)))))), 4'(3(0(z0))), 3'(0(z0)), 0'(z0))
5'(1(5(2(0(z0))))) → c46(3'(5(0(5(z0)))), 5'(0(5(z0))), 0'(5(z0)), 5'(z0))
5'(4(1(0(5(z0))))) → c47(4'(1(3(5(5(0(z0)))))), 3'(5(5(0(z0)))), 5'(5(0(z0))), 5'(0(z0)), 0'(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(0(1(2(z0)))) → 0(2(1(3(3(0(z0))))))
0(1(0(4(z0)))) → 0(1(3(0(4(z0)))))
0(1(0(5(z0)))) → 0(1(3(5(0(z0)))))
0(1(5(0(z0)))) → 0(1(3(5(0(z0)))))
0(3(1(0(z0)))) → 0(1(3(5(0(z0)))))
0(0(4(1(0(z0))))) → 0(4(1(3(0(0(z0))))))
0(1(2(0(5(z0))))) → 0(3(0(5(1(2(z0))))))
0(1(3(1(2(z0))))) → 3(0(2(2(1(1(z0))))))
0(1(5(0(4(z0))))) → 0(4(1(3(5(0(z0))))))
0(1(5(3(5(z0))))) → 0(1(3(5(3(5(z0))))))
0(2(0(3(4(z0))))) → 0(4(5(2(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(1(3(5(5(2(z0))))))
0(2(4(1(2(z0))))) → 0(2(1(1(4(2(z0))))))
0(2(5(0(2(z0))))) → 0(0(3(5(2(2(z0))))))
0(2(5(5(0(z0))))) → 0(0(2(5(1(5(z0))))))
0(3(1(5(0(z0))))) → 1(3(0(5(3(0(z0))))))
0(5(3(2(0(z0))))) → 0(0(2(1(3(5(z0))))))
3(1(0(2(z0)))) → 1(3(5(0(2(z0)))))
3(1(0(2(z0)))) → 3(2(1(3(0(z0)))))
3(1(0(5(z0)))) → 1(3(5(3(0(z0)))))
3(1(2(0(z0)))) → 2(1(3(3(0(z0)))))
3(1(2(0(z0)))) → 3(0(2(1(4(z0)))))
3(1(2(0(z0)))) → 3(0(3(2(1(z0)))))
3(1(2(0(z0)))) → 3(3(2(1(0(z0)))))
3(1(2(0(z0)))) → 3(5(2(1(0(z0)))))
3(1(2(2(z0)))) → 3(5(2(2(1(z0)))))
3(4(2(0(z0)))) → 3(3(2(4(0(z0)))))
3(1(0(5(2(z0))))) → 2(4(1(3(5(0(z0))))))
3(1(3(0(2(z0))))) → 2(1(3(3(3(0(z0))))))
3(1(3(2(0(z0))))) → 3(1(3(0(5(2(z0))))))
3(1(4(1(2(z0))))) → 1(4(3(2(2(1(z0))))))
3(1(4(2(0(z0))))) → 2(1(3(3(0(4(z0))))))
3(1(5(0(2(z0))))) → 2(5(1(3(0(5(z0))))))
3(3(1(0(0(z0))))) → 5(1(3(3(0(0(z0))))))
3(4(0(2(0(z0))))) → 3(0(0(2(1(4(z0))))))
3(4(2(3(2(z0))))) → 3(3(2(5(4(2(z0))))))
4(0(1(0(z0)))) → 1(3(0(4(0(z0)))))
4(3(1(0(2(z0))))) → 4(2(1(3(0(1(z0))))))
4(3(1(2(0(z0))))) → 1(3(0(1(4(2(z0))))))
4(5(5(1(2(z0))))) → 5(4(5(2(1(1(z0))))))
4(5(5(5(0(z0))))) → 5(5(1(5(0(4(z0))))))
5(1(0(5(z0)))) → 1(3(3(5(5(0(z0))))))
5(2(5(0(z0)))) → 5(2(3(5(0(z0)))))
5(3(1(0(z0)))) → 0(1(3(5(5(z0)))))
5(1(0(1(2(z0))))) → 2(1(1(3(5(0(z0))))))
5(1(1(0(4(z0))))) → 5(1(1(4(3(0(z0))))))
5(1(5(2(0(z0))))) → 2(1(3(5(0(5(z0))))))
5(4(1(0(5(z0))))) → 4(1(3(5(5(0(z0))))))
Tuples:
3'(1(2(2(z0)))) → c25(3'(5(2(2(1(z0))))), 5'(2(2(1(z0)))))
S tuples:
3'(1(2(2(z0)))) → c25(3'(5(2(2(1(z0))))), 5'(2(2(1(z0)))))
K tuples:none
Defined Rule Symbols:
0, 3, 4, 5
Defined Pair Symbols:
3'
Compound Symbols:
c25
(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 1 of 1 dangling nodes:
3'(1(2(2(z0)))) → c25(3'(5(2(2(1(z0))))), 5'(2(2(1(z0)))))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(0(1(2(z0)))) → 0(2(1(3(3(0(z0))))))
0(1(0(4(z0)))) → 0(1(3(0(4(z0)))))
0(1(0(5(z0)))) → 0(1(3(5(0(z0)))))
0(1(5(0(z0)))) → 0(1(3(5(0(z0)))))
0(3(1(0(z0)))) → 0(1(3(5(0(z0)))))
0(0(4(1(0(z0))))) → 0(4(1(3(0(0(z0))))))
0(1(2(0(5(z0))))) → 0(3(0(5(1(2(z0))))))
0(1(3(1(2(z0))))) → 3(0(2(2(1(1(z0))))))
0(1(5(0(4(z0))))) → 0(4(1(3(5(0(z0))))))
0(1(5(3(5(z0))))) → 0(1(3(5(3(5(z0))))))
0(2(0(3(4(z0))))) → 0(4(5(2(3(0(z0))))))
0(2(3(1(5(z0))))) → 0(1(3(5(5(2(z0))))))
0(2(4(1(2(z0))))) → 0(2(1(1(4(2(z0))))))
0(2(5(0(2(z0))))) → 0(0(3(5(2(2(z0))))))
0(2(5(5(0(z0))))) → 0(0(2(5(1(5(z0))))))
0(3(1(5(0(z0))))) → 1(3(0(5(3(0(z0))))))
0(5(3(2(0(z0))))) → 0(0(2(1(3(5(z0))))))
3(1(0(2(z0)))) → 1(3(5(0(2(z0)))))
3(1(0(2(z0)))) → 3(2(1(3(0(z0)))))
3(1(0(5(z0)))) → 1(3(5(3(0(z0)))))
3(1(2(0(z0)))) → 2(1(3(3(0(z0)))))
3(1(2(0(z0)))) → 3(0(2(1(4(z0)))))
3(1(2(0(z0)))) → 3(0(3(2(1(z0)))))
3(1(2(0(z0)))) → 3(3(2(1(0(z0)))))
3(1(2(0(z0)))) → 3(5(2(1(0(z0)))))
3(1(2(2(z0)))) → 3(5(2(2(1(z0)))))
3(4(2(0(z0)))) → 3(3(2(4(0(z0)))))
3(1(0(5(2(z0))))) → 2(4(1(3(5(0(z0))))))
3(1(3(0(2(z0))))) → 2(1(3(3(3(0(z0))))))
3(1(3(2(0(z0))))) → 3(1(3(0(5(2(z0))))))
3(1(4(1(2(z0))))) → 1(4(3(2(2(1(z0))))))
3(1(4(2(0(z0))))) → 2(1(3(3(0(4(z0))))))
3(1(5(0(2(z0))))) → 2(5(1(3(0(5(z0))))))
3(3(1(0(0(z0))))) → 5(1(3(3(0(0(z0))))))
3(4(0(2(0(z0))))) → 3(0(0(2(1(4(z0))))))
3(4(2(3(2(z0))))) → 3(3(2(5(4(2(z0))))))
4(0(1(0(z0)))) → 1(3(0(4(0(z0)))))
4(3(1(0(2(z0))))) → 4(2(1(3(0(1(z0))))))
4(3(1(2(0(z0))))) → 1(3(0(1(4(2(z0))))))
4(5(5(1(2(z0))))) → 5(4(5(2(1(1(z0))))))
4(5(5(5(0(z0))))) → 5(5(1(5(0(4(z0))))))
5(1(0(5(z0)))) → 1(3(3(5(5(0(z0))))))
5(2(5(0(z0)))) → 5(2(3(5(0(z0)))))
5(3(1(0(z0)))) → 0(1(3(5(5(z0)))))
5(1(0(1(2(z0))))) → 2(1(1(3(5(0(z0))))))
5(1(1(0(4(z0))))) → 5(1(1(4(3(0(z0))))))
5(1(5(2(0(z0))))) → 2(1(3(5(0(5(z0))))))
5(4(1(0(5(z0))))) → 4(1(3(5(5(0(z0))))))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
0, 3, 4, 5
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))